
; Copyright (c) 2015 Microsoft Corporation
(set-option :auto-config true)
(set-option :produce-models true)
(set-option :smt.ematching false)
(declare-datatypes () ((T t0 t1 t2)))
(declare-fun g_ (T) Bool)
(declare-fun sends_ (T) Bool)
(declare-fun tok_ (T) Bool)
(declare-fun tau (T Bool Bool) T)
(assert (forall ((?r_ Bool)) (=> (and (tok_ t0) (not (sends_ t0))) (tok_ (tau t0 ?r_ false)))))
(assert (forall ((?r_ Bool)) (=> (sends_ t0) (tok_ t0))))
(assert (forall ((?r_ Bool)) (=> (sends_ t0) (not (tok_ (tau t0 ?r_ false))))))
(assert (forall ((?r_ Bool)) (tok_ (tau t0 ?r_ true))))
(assert (forall ((?r_ Bool)) (=> (not (tok_ t0)) (not (tok_ (tau t0 ?r_ false))))))
(assert (forall ((?r_ Bool)) (=> (and (tok_ t1) (not (sends_ t1))) (tok_ (tau t1 ?r_ false)))))
(assert (forall ((?r_ Bool)) (=> (sends_ t1) (tok_ t1))))
(assert (forall ((?r_ Bool)) (=> (sends_ t1) (not (tok_ (tau t1 ?r_ false))))))
(assert (forall ((?r_ Bool)) (tok_ (tau t1 ?r_ true))))
(assert (forall ((?r_ Bool)) (=> (not (tok_ t1)) (not (tok_ (tau t1 ?r_ false))))))
(assert (forall ((?r_ Bool)) (=> (and (tok_ t2) (not (sends_ t2))) (tok_ (tau t2 ?r_ false)))))
(assert (forall ((?r_ Bool)) (=> (sends_ t2) (tok_ t2))))
(assert (forall ((?r_ Bool)) (=> (sends_ t2) (not (tok_ (tau t2 ?r_ false))))))
(assert (forall ((?r_ Bool)) (tok_ (tau t2 ?r_ true))))
(assert (forall ((?r_ Bool)) (=> (not (tok_ t2)) (not (tok_ (tau t2 ?r_ false))))))
(define-fun equal_bits_0 ((y0 Bool) (x0 Bool)) Bool
(= x0 y0)
)
(define-fun equal_to_prev_0 ((proc0 Bool) (sch0 Bool)) Bool
(or (and (equal_bits_0 proc0 false) (equal_bits_0 sch0 true))
(and (equal_bits_0 proc0 true) (equal_bits_0 sch0 false)))
)
(define-fun is_active_0 ((proc0 Bool) (sch0 Bool) (prev_ Bool)) Bool
(or (and (not prev_) (equal_bits_0 sch0 proc0)) (and prev_ (equal_to_prev_0 sch0 proc0)))
)
(define-fun tau_sch_0 ((state T) (r_ Bool) (proc0 Bool) (sch0 Bool) (prev_ Bool)) T
(ite (is_active_0 proc0 sch0 prev_) (tau state r_ prev_) state)
)
(assert (tok_ t1))
(assert (not (tok_ t0)))
(declare-datatypes () ((Q0 q0_T0_init q0_accept_all)))
(declare-fun laB_0 (Q0 T T) Bool)
(declare-fun laC_0 (Q0 T T) Int)
(assert (laB_0 q0_T0_init t1 t0))
(assert (laB_0 q0_T0_init t0 t1))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t0 t0) (and (g_ t0) (not (g_ t0))) )  (laB_0 q0_T0_init (tau_sch_0 t0 ?r0 false ?sch0 (sends_ t0)) (tau_sch_0 t0 ?r1 true ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t0 t0)  (not (g_ t0))  )  (laB_0 q0_T0_init (tau_sch_0 t0 ?r0 false ?sch0 (sends_ t0)) (tau_sch_0 t0 ?r1 true ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t0 t0) (and (g_ t0) (g_ t0)) )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t0 t1) (and (g_ t0) (not (g_ t1))) )  (laB_0 q0_T0_init (tau_sch_0 t0 ?r0 false ?sch0 (sends_ t1)) (tau_sch_0 t1 ?r1 true ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t0 t1)  (not (g_ t0))  )  (laB_0 q0_T0_init (tau_sch_0 t0 ?r0 false ?sch0 (sends_ t1)) (tau_sch_0 t1 ?r1 true ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t0 t1) (and (g_ t0) (g_ t1)) )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t0 t2) (and (g_ t0) (not (g_ t2))) )  (laB_0 q0_T0_init (tau_sch_0 t0 ?r0 false ?sch0 (sends_ t2)) (tau_sch_0 t2 ?r1 true ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t0 t2)  (not (g_ t0))  )  (laB_0 q0_T0_init (tau_sch_0 t0 ?r0 false ?sch0 (sends_ t2)) (tau_sch_0 t2 ?r1 true ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t0 t2) (and (g_ t0) (g_ t2)) )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t1 t0) (and (g_ t1) (not (g_ t0))) )  (laB_0 q0_T0_init (tau_sch_0 t1 ?r0 false ?sch0 (sends_ t0)) (tau_sch_0 t0 ?r1 true ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t1 t0)  (not (g_ t1))  )  (laB_0 q0_T0_init (tau_sch_0 t1 ?r0 false ?sch0 (sends_ t0)) (tau_sch_0 t0 ?r1 true ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t1 t0) (and (g_ t1) (g_ t0)) )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t1 t1) (and (g_ t1) (not (g_ t1))) )  (laB_0 q0_T0_init (tau_sch_0 t1 ?r0 false ?sch0 (sends_ t1)) (tau_sch_0 t1 ?r1 true ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t1 t1)  (not (g_ t1))  )  (laB_0 q0_T0_init (tau_sch_0 t1 ?r0 false ?sch0 (sends_ t1)) (tau_sch_0 t1 ?r1 true ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t1 t1) (and (g_ t1) (g_ t1)) )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t1 t2) (and (g_ t1) (not (g_ t2))) )  (laB_0 q0_T0_init (tau_sch_0 t1 ?r0 false ?sch0 (sends_ t2)) (tau_sch_0 t2 ?r1 true ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t1 t2)  (not (g_ t1))  )  (laB_0 q0_T0_init (tau_sch_0 t1 ?r0 false ?sch0 (sends_ t2)) (tau_sch_0 t2 ?r1 true ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t1 t2) (and (g_ t1) (g_ t2)) )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t2 t0) (and (g_ t2) (not (g_ t0))) )  (laB_0 q0_T0_init (tau_sch_0 t2 ?r0 false ?sch0 (sends_ t0)) (tau_sch_0 t0 ?r1 true ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t2 t0)  (not (g_ t2))  )  (laB_0 q0_T0_init (tau_sch_0 t2 ?r0 false ?sch0 (sends_ t0)) (tau_sch_0 t0 ?r1 true ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t2 t0) (and (g_ t2) (g_ t0)) )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t2 t1) (and (g_ t2) (not (g_ t1))) )  (laB_0 q0_T0_init (tau_sch_0 t2 ?r0 false ?sch0 (sends_ t1)) (tau_sch_0 t1 ?r1 true ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t2 t1)  (not (g_ t2))  )  (laB_0 q0_T0_init (tau_sch_0 t2 ?r0 false ?sch0 (sends_ t1)) (tau_sch_0 t1 ?r1 true ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t2 t1) (and (g_ t2) (g_ t1)) )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t2 t2) (and (g_ t2) (not (g_ t2))) )  (laB_0 q0_T0_init (tau_sch_0 t2 ?r0 false ?sch0 (sends_ t2)) (tau_sch_0 t2 ?r1 true ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t2 t2)  (not (g_ t2))  )  (laB_0 q0_T0_init (tau_sch_0 t2 ?r0 false ?sch0 (sends_ t2)) (tau_sch_0 t2 ?r1 true ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_T0_init t2 t2) (and (g_ t2) (g_ t2)) )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_accept_all t0 t0)  )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_accept_all t0 t1)  )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_accept_all t0 t2)  )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_accept_all t1 t0)  )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_accept_all t1 t1)  )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_accept_all t1 t2)  )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_accept_all t2 t0)  )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_accept_all t2 t1)  )   false  )))
(assert (forall ((?sch0 Bool) (?r0 Bool) (?r1 Bool)) (=> (and (laB_0 q0_accept_all t2 t2)  )   false  )))




(define-fun equal_bits_1 ((y0 Bool) (x0 Bool)) Bool
(= x0 y0)
)
(define-fun equal_to_prev_1 ((proc0 Bool) (sch0 Bool)) Bool
(or (and (equal_bits_1 proc0 false) (equal_bits_1 sch0 true)))
)
(define-fun is_active_1 ((proc0 Bool) (sch0 Bool) (prev_ Bool)) Bool
(or (and (not prev_) (equal_bits_1 sch0 proc0)) (and prev_ (equal_to_prev_1 sch0 proc0)))
)
(define-fun tau_sch_1 ((state T) (r_ Bool) (proc0 Bool) (sch0 Bool) (prev_ Bool)) T
(ite (is_active_1 proc0 sch0 prev_) (tau state r_ prev_) state)
)

(assert (tok_ t1))

(declare-datatypes () ((Q1
q1_T0_S10
q1_accept_S10
q1_T5_S9
q1_accept_S7
q1_T1_S19
q1_T0_S16
q1_T3_S29
q1_T0_S18
q1_T1_S27
q1_T1_S31
q1_T1_S41
q1_accept_S41
q1_T5_S18
q1_T6_S19
q1_T0_S31
q1_T1_S23
q1_T0_S40
q1_T0_S29
q1_T0_S7
q1_T1_S16
q1_T0_S23
q1_T2_S23
q1_T2_S21
q1_T1_S18
q1_T3_S31
q1_T6_S11
q1_T0_S21
q1_T0_S9
q1_T0_S27
q1_T0_S35
q1_T1_S17
q1_T0_S17
q1_T0_S11
q1_T4_S8
q1_T0_S8
q1_T0_init
q1_T0_S37
q1_T1_S35
q1_accept_S25
q1_T0_S34
q1_accept_S34
q1_T0_S19
q1_T4_S17
q1_T1_S37
q1_T0_S25)))

(declare-fun laB_1 (Q1 T) Bool)
(declare-fun laC_1 (Q1 T) Int)

; bug?
; beginning of bas_assertions section
; 

(assert (laB_1 q1_T0_init t1))
(assert (laB_1 q1_T0_init t0))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t0) (and (not (sends_ t0)) (not (tok_ t0))) )  (and (laB_1 q1_T1_S37 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (>= (laC_1 q1_T1_S37 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S10 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t0) (and (not (sends_ t0)) (not (tok_ t0))) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S10 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t0) (and (not (sends_ t0)) (tok_ t0)) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S10 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t0) (and (not (sends_ t0)) (tok_ t0)) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S10 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t0) (and (not (sends_ t0)) (not (tok_ t0))) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S10 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t0) (and (not (sends_ t0)) (not (tok_ t0))) )  (and (laB_1 q1_T0_S37 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S37 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S10 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t1) (and (not (sends_ t1)) (not (tok_ t1))) )  (and (laB_1 q1_T1_S37 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (>= (laC_1 q1_T1_S37 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S10 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t1) (and (not (sends_ t1)) (not (tok_ t1))) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S10 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t1) (and (not (sends_ t1)) (tok_ t1)) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S10 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t1) (and (not (sends_ t1)) (tok_ t1)) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S10 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t1) (and (not (sends_ t1)) (not (tok_ t1))) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S10 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t1) (and (not (sends_ t1)) (not (tok_ t1))) )  (and (laB_1 q1_T0_S37 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S37 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S10 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t2) (and (not (sends_ t2)) (not (tok_ t2))) )  (and (laB_1 q1_T1_S37 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (>= (laC_1 q1_T1_S37 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S10 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t2) (and (not (sends_ t2)) (not (tok_ t2))) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S10 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t2) (and (not (sends_ t2)) (tok_ t2)) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S10 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t2) (and (not (sends_ t2)) (tok_ t2)) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S10 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t2) (and (not (sends_ t2)) (not (tok_ t2))) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S10 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S10 t2) (and (not (sends_ t2)) (not (tok_ t2))) )  (and (laB_1 q1_T0_S37 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S37 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S10 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t0) (and (not (sends_ t0)) (not (tok_ t0))) )  (and (laB_1 q1_T1_S37 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (>= (laC_1 q1_T1_S37 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_accept_S10 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t0) (and (not (sends_ t0)) (not (tok_ t0))) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_accept_S10 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t0) (and (not (sends_ t0)) (tok_ t0)) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_accept_S10 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t0) (and (not (sends_ t0)) (tok_ t0)) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_accept_S10 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t0) (and (not (sends_ t0)) (not (tok_ t0))) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_accept_S10 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t0) (and (not (sends_ t0)) (not (tok_ t0))) )  (and (laB_1 q1_T0_S37 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S37 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_accept_S10 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t1) (and (not (sends_ t1)) (not (tok_ t1))) )  (and (laB_1 q1_T1_S37 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (>= (laC_1 q1_T1_S37 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_accept_S10 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t1) (and (not (sends_ t1)) (not (tok_ t1))) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_accept_S10 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t1) (and (not (sends_ t1)) (tok_ t1)) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_accept_S10 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t1) (and (not (sends_ t1)) (tok_ t1)) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_accept_S10 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t1) (and (not (sends_ t1)) (not (tok_ t1))) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_accept_S10 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t1) (and (not (sends_ t1)) (not (tok_ t1))) )  (and (laB_1 q1_T0_S37 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S37 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_accept_S10 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t2) (and (not (sends_ t2)) (not (tok_ t2))) )  (and (laB_1 q1_T1_S37 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (>= (laC_1 q1_T1_S37 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_accept_S10 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t2) (and (not (sends_ t2)) (not (tok_ t2))) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_accept_S10 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t2) (and (not (sends_ t2)) (tok_ t2)) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_accept_S10 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t2) (and (not (sends_ t2)) (tok_ t2)) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_accept_S10 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t2) (and (not (sends_ t2)) (not (tok_ t2))) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_accept_S10 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S10 t2) (and (not (sends_ t2)) (not (tok_ t2))) )  (and (laB_1 q1_T0_S37 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S37 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_accept_S10 t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_T0_S40 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t0)  (tok_ t0)  )  (laB_1 q1_T5_S9 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_accept_S41 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t0)  (not (tok_ t0))  )  (laB_1 q1_T5_S18 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t0) (and (tok_ t0) (g_ t0)) )  (laB_1 q1_T0_S40 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t0)  (not (tok_ t0))  )  (laB_1 q1_T5_S9 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_T0_S40 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t1)  (tok_ t1)  )  (laB_1 q1_T5_S9 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_accept_S41 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t1)  (not (tok_ t1))  )  (laB_1 q1_T5_S18 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t1) (and (tok_ t1) (g_ t1)) )  (laB_1 q1_T0_S40 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t1)  (not (tok_ t1))  )  (laB_1 q1_T5_S9 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_T0_S40 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t2)  (tok_ t2)  )  (laB_1 q1_T5_S9 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_accept_S41 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t2)  (not (tok_ t2))  )  (laB_1 q1_T5_S18 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t2) (and (tok_ t2) (g_ t2)) )  (laB_1 q1_T0_S40 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S9 t2)  (not (tok_ t2))  )  (laB_1 q1_T5_S9 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t0)  (not (tok_ t0))  )  (and (laB_1 q1_T1_S16 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (>= (laC_1 q1_T1_S16 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_accept_S7 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t0)  (not (tok_ t0))  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S7 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_accept_S7 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t0)  (not (tok_ t0))  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_accept_S7 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t0)  (not (tok_ t0))  )  (and (laB_1 q1_T0_S16 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S16 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_accept_S7 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t0)  (tok_ t0)  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S7 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_accept_S7 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t0)  (tok_ t0)  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_accept_S7 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t1)  (not (tok_ t1))  )  (and (laB_1 q1_T1_S16 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (>= (laC_1 q1_T1_S16 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_accept_S7 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t1)  (not (tok_ t1))  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S7 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_accept_S7 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t1)  (not (tok_ t1))  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_accept_S7 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t1)  (not (tok_ t1))  )  (and (laB_1 q1_T0_S16 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S16 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_accept_S7 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t1)  (tok_ t1)  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S7 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_accept_S7 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t1)  (tok_ t1)  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_accept_S7 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t2)  (not (tok_ t2))  )  (and (laB_1 q1_T1_S16 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (>= (laC_1 q1_T1_S16 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_accept_S7 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t2)  (not (tok_ t2))  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S7 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_accept_S7 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t2)  (not (tok_ t2))  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_accept_S7 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t2)  (not (tok_ t2))  )  (and (laB_1 q1_T0_S16 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S16 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_accept_S7 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t2)  (tok_ t2)  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S7 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_accept_S7 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S7 t2)  (tok_ t2)  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_accept_S7 t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S19 t0) (and (not (sends_ t0)) (tok_ t0)) )  (laB_1 q1_T1_S37 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S19 t0)  )  (laB_1 q1_T1_S19 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S19 t0)  (not (tok_ t0))  )  (laB_1 q1_T6_S11 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S19 t1) (and (not (sends_ t1)) (tok_ t1)) )  (laB_1 q1_T1_S37 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S19 t1)  )  (laB_1 q1_T1_S19 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S19 t1)  (not (tok_ t1))  )  (laB_1 q1_T6_S11 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S19 t2) (and (not (sends_ t2)) (tok_ t2)) )  (laB_1 q1_T1_S37 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S19 t2)  )  (laB_1 q1_T1_S19 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S19 t2)  (not (tok_ t2))  )  (laB_1 q1_T6_S11 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S16 t0)  )  (and (laB_1 q1_T1_S16 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (>= (laC_1 q1_T1_S16 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S16 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S16 t0)  (not (tok_ t0))  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S16 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S16 t0)  (not (tok_ t0))  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S7 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S16 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S16 t0)  )  (and (laB_1 q1_T0_S16 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S16 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S16 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S16 t1)  )  (and (laB_1 q1_T1_S16 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (>= (laC_1 q1_T1_S16 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S16 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S16 t1)  (not (tok_ t1))  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S16 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S16 t1)  (not (tok_ t1))  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S7 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S16 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S16 t1)  )  (and (laB_1 q1_T0_S16 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S16 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S16 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S16 t2)  )  (and (laB_1 q1_T1_S16 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (>= (laC_1 q1_T1_S16 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S16 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S16 t2)  (not (tok_ t2))  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S16 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S16 t2)  (not (tok_ t2))  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S7 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S16 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S16 t2)  )  (and (laB_1 q1_T0_S16 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S16 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S16 t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S29 t0) (and (not (tok_ t0)) (not (g_ t0))) (is_active_1 false ?sch0 (sends_ t0)))  (laB_1 q1_accept_S25 (tau_sch_1 t0 true false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S29 t0)  (tok_ t0)  )  (laB_1 q1_T3_S29 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S29 t0) (and (not (tok_ t0)) (not (g_ t0))) (is_active_1 false ?sch0 (sends_ t0)))  (laB_1 q1_T0_S27 (tau_sch_1 t0 true false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S29 t0)  (not (tok_ t0))  )  (laB_1 q1_T3_S31 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S29 t0) (and (tok_ t0) (not (g_ t0))) (is_active_1 false ?sch0 (sends_ t0)))  (laB_1 q1_accept_S25 (tau_sch_1 t0 true false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S29 t0)  (not (tok_ t0))  )  (laB_1 q1_T3_S29 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S29 t1) (and (not (tok_ t1)) (not (g_ t1))) (is_active_1 false ?sch0 (sends_ t1)))  (laB_1 q1_accept_S25 (tau_sch_1 t1 true false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S29 t1)  (tok_ t1)  )  (laB_1 q1_T3_S29 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S29 t1) (and (not (tok_ t1)) (not (g_ t1))) (is_active_1 false ?sch0 (sends_ t1)))  (laB_1 q1_T0_S27 (tau_sch_1 t1 true false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S29 t1)  (not (tok_ t1))  )  (laB_1 q1_T3_S31 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S29 t1) (and (tok_ t1) (not (g_ t1))) (is_active_1 false ?sch0 (sends_ t1)))  (laB_1 q1_accept_S25 (tau_sch_1 t1 true false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S29 t1)  (not (tok_ t1))  )  (laB_1 q1_T3_S29 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S29 t2) (and (not (tok_ t2)) (not (g_ t2))) (is_active_1 false ?sch0 (sends_ t2)))  (laB_1 q1_accept_S25 (tau_sch_1 t2 true false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S29 t2)  (tok_ t2)  )  (laB_1 q1_T3_S29 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S29 t2) (and (not (tok_ t2)) (not (g_ t2))) (is_active_1 false ?sch0 (sends_ t2)))  (laB_1 q1_T0_S27 (tau_sch_1 t2 true false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S29 t2)  (not (tok_ t2))  )  (laB_1 q1_T3_S31 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S29 t2) (and (tok_ t2) (not (g_ t2))) (is_active_1 false ?sch0 (sends_ t2)))  (laB_1 q1_accept_S25 (tau_sch_1 t2 true false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S29 t2)  (not (tok_ t2))  )  (laB_1 q1_T3_S29 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_T0_S40 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t0)  (not (tok_ t0))  )  (laB_1 q1_T5_S9 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t0)  (g_ t0)  )  (laB_1 q1_accept_S41 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t0)  (not (tok_ t0))  )  (laB_1 q1_T0_S9 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t0)  )  (laB_1 q1_T0_S18 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t0)  )  (laB_1 q1_T1_S18 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t0)  (g_ t0)  )  (laB_1 q1_T1_S41 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_T0_S40 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t1)  (not (tok_ t1))  )  (laB_1 q1_T5_S9 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t1)  (g_ t1)  )  (laB_1 q1_accept_S41 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t1)  (not (tok_ t1))  )  (laB_1 q1_T0_S9 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t1)  )  (laB_1 q1_T0_S18 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t1)  )  (laB_1 q1_T1_S18 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t1)  (g_ t1)  )  (laB_1 q1_T1_S41 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_T0_S40 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t2)  (not (tok_ t2))  )  (laB_1 q1_T5_S9 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t2)  (g_ t2)  )  (laB_1 q1_accept_S41 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t2)  (not (tok_ t2))  )  (laB_1 q1_T0_S9 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t2)  )  (laB_1 q1_T0_S18 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t2)  )  (laB_1 q1_T1_S18 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S18 t2)  (g_ t2)  )  (laB_1 q1_T1_S41 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S27 t0)  (not (g_ t0))  )  (and (laB_1 q1_T1_S27 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) (>= (laC_1 q1_T1_S27 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) (laC_1 q1_T1_S27 t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S27 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) (> (laC_1 q1_accept_S25 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) (laC_1 q1_T1_S27 t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S27 t1)  (not (g_ t1))  )  (and (laB_1 q1_T1_S27 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) (>= (laC_1 q1_T1_S27 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) (laC_1 q1_T1_S27 t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S27 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) (> (laC_1 q1_accept_S25 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) (laC_1 q1_T1_S27 t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S27 t2)  (not (g_ t2))  )  (and (laB_1 q1_T1_S27 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) (>= (laC_1 q1_T1_S27 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) (laC_1 q1_T1_S27 t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S27 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) (> (laC_1 q1_accept_S25 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) (laC_1 q1_T1_S27 t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S31 t0) (and (not (tok_ t0)) (not (g_ t0))) (is_active_1 false ?sch0 (sends_ t0)))  (laB_1 q1_accept_S25 (tau_sch_1 t0 true false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S31 t0)  )  (laB_1 q1_T1_S31 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S31 t0)  (not (g_ t0))  (is_active_1 false ?sch0 (sends_ t0)))  (laB_1 q1_T1_S27 (tau_sch_1 t0 true false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S31 t0)  (not (tok_ t0))  )  (laB_1 q1_T3_S29 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S31 t1) (and (not (tok_ t1)) (not (g_ t1))) (is_active_1 false ?sch0 (sends_ t1)))  (laB_1 q1_accept_S25 (tau_sch_1 t1 true false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S31 t1)  )  (laB_1 q1_T1_S31 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S31 t1)  (not (g_ t1))  (is_active_1 false ?sch0 (sends_ t1)))  (laB_1 q1_T1_S27 (tau_sch_1 t1 true false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S31 t1)  (not (tok_ t1))  )  (laB_1 q1_T3_S29 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S31 t2) (and (not (tok_ t2)) (not (g_ t2))) (is_active_1 false ?sch0 (sends_ t2)))  (laB_1 q1_accept_S25 (tau_sch_1 t2 true false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S31 t2)  )  (laB_1 q1_T1_S31 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S31 t2)  (not (g_ t2))  (is_active_1 false ?sch0 (sends_ t2)))  (laB_1 q1_T1_S27 (tau_sch_1 t2 true false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S31 t2)  (not (tok_ t2))  )  (laB_1 q1_T3_S29 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S41 t0)  (not (g_ t0))  )  (laB_1 q1_T1_S17 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S41 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T4_S8 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S41 t1)  (not (g_ t1))  )  (laB_1 q1_T1_S17 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S41 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T4_S8 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S41 t2)  (not (g_ t2))  )  (laB_1 q1_T1_S17 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S41 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T4_S8 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (=> (and (laB_1 q1_accept_S41 t0)  (not (g_ t0))  )  (laB_1 q1_T1_S17 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_accept_S41 t0)  (not (g_ t0))  )  (laB_1 q1_T0_S17 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_accept_S41 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T4_S8 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_accept_S41 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T0_S8 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_accept_S41 t1)  (not (g_ t1))  )  (laB_1 q1_T1_S17 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_accept_S41 t1)  (not (g_ t1))  )  (laB_1 q1_T0_S17 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_accept_S41 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T4_S8 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_accept_S41 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T0_S8 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_accept_S41 t2)  (not (g_ t2))  )  (laB_1 q1_T1_S17 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_accept_S41 t2)  (not (g_ t2))  )  (laB_1 q1_T0_S17 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_accept_S41 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T4_S8 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_accept_S41 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T0_S8 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S18 t0)  (g_ t0)  )  (laB_1 q1_accept_S41 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S18 t0)  (not (tok_ t0))  )  (laB_1 q1_T5_S9 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S18 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_T0_S40 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S18 t0)  )  (laB_1 q1_T5_S18 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S18 t1)  (g_ t1)  )  (laB_1 q1_accept_S41 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S18 t1)  (not (tok_ t1))  )  (laB_1 q1_T5_S9 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S18 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_T0_S40 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S18 t1)  )  (laB_1 q1_T5_S18 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S18 t2)  (g_ t2)  )  (laB_1 q1_accept_S41 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S18 t2)  (not (tok_ t2))  )  (laB_1 q1_T5_S9 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S18 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_T0_S40 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T5_S18 t2)  )  (laB_1 q1_T5_S18 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S19 t0) (and (not (sends_ t0)) (tok_ t0)) )  (laB_1 q1_T0_S37 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S19 t0)  )  (laB_1 q1_T6_S19 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S19 t0)  (not (tok_ t0))  )  (laB_1 q1_T6_S11 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S19 t1) (and (not (sends_ t1)) (tok_ t1)) )  (laB_1 q1_T0_S37 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S19 t1)  )  (laB_1 q1_T6_S19 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S19 t1)  (not (tok_ t1))  )  (laB_1 q1_T6_S11 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S19 t2) (and (not (sends_ t2)) (tok_ t2)) )  (laB_1 q1_T0_S37 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S19 t2)  )  (laB_1 q1_T6_S19 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S19 t2)  (not (tok_ t2))  )  (laB_1 q1_T6_S11 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S31 t0) (and (not (tok_ t0)) (not (g_ t0))) (is_active_1 false true (sends_ t0)))  (laB_1 q1_T0_S25 (tau_sch_1 t0 true false true (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S31 t0)  (not (tok_ t0))  )  (laB_1 q1_T3_S29 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_S31 t0)  (not (g_ t0))  (is_active_1 false true (sends_ t0)))  (laB_1 q1_T0_S27 (tau_sch_1 t0 true false true (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S31 t0)  (not (tok_ t0))  )  (laB_1 q1_T0_S29 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_S31 t0) (and (not (tok_ t0)) (not (g_ t0))) (is_active_1 false false (sends_ t0)))  (laB_1 q1_accept_S25 (tau_sch_1 t0 true false false (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S31 t0)  )  (laB_1 q1_T0_S31 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S31 t0)  )  (laB_1 q1_T1_S31 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_S31 t0)  (not (g_ t0))  (is_active_1 false false (sends_ t0)))  (laB_1 q1_T1_S27 (tau_sch_1 t0 true false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S31 t1) (and (not (tok_ t1)) (not (g_ t1))) (is_active_1 false true (sends_ t1)))  (laB_1 q1_T0_S25 (tau_sch_1 t1 true false true (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S31 t1)  (not (tok_ t1))  )  (laB_1 q1_T3_S29 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_S31 t1)  (not (g_ t1))  (is_active_1 false true (sends_ t1)))  (laB_1 q1_T0_S27 (tau_sch_1 t1 true false true (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S31 t1)  (not (tok_ t1))  )  (laB_1 q1_T0_S29 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_S31 t1) (and (not (tok_ t1)) (not (g_ t1))) (is_active_1 false false (sends_ t1)))  (laB_1 q1_accept_S25 (tau_sch_1 t1 true false false (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S31 t1)  )  (laB_1 q1_T0_S31 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S31 t1)  )  (laB_1 q1_T1_S31 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_S31 t1)  (not (g_ t1))  (is_active_1 false false (sends_ t1)))  (laB_1 q1_T1_S27 (tau_sch_1 t1 true false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S31 t2) (and (not (tok_ t2)) (not (g_ t2))) (is_active_1 false true (sends_ t2)))  (laB_1 q1_T0_S25 (tau_sch_1 t2 true false true (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S31 t2)  (not (tok_ t2))  )  (laB_1 q1_T3_S29 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S31 t2)  (not (g_ t2))  (is_active_1 false true (sends_ t2)))  (laB_1 q1_T0_S27 (tau_sch_1 t2 true false true (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S31 t2)  (not (tok_ t2))  )  (laB_1 q1_T0_S29 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S31 t2) (and (not (tok_ t2)) (not (g_ t2))) (is_active_1 false false (sends_ t2)))  (laB_1 q1_accept_S25 (tau_sch_1 t2 true false false (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S31 t2)  )  (laB_1 q1_T0_S31 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S31 t2)  )  (laB_1 q1_T1_S31 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S31 t2)  (not (g_ t2))  (is_active_1 false false (sends_ t2)))  (laB_1 q1_T1_S27 (tau_sch_1 t2 true false false (sends_ t2))) ))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S23 t0) (and (not (tok_ t0)) (g_ t0)) (is_active_1 false ?sch0 (sends_ t0)))  (laB_1 q1_accept_S34 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S23 t0)  )  (laB_1 q1_T1_S23 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S23 t0)  (g_ t0)  (is_active_1 false ?sch0 (sends_ t0)))  (laB_1 q1_T1_S35 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S23 t0)  (not (tok_ t0))  )  (laB_1 q1_T2_S21 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S23 t1) (and (not (tok_ t1)) (g_ t1)) (is_active_1 false ?sch0 (sends_ t1)))  (laB_1 q1_accept_S34 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S23 t1)  )  (laB_1 q1_T1_S23 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S23 t1)  (g_ t1)  (is_active_1 false ?sch0 (sends_ t1)))  (laB_1 q1_T1_S35 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S23 t1)  (not (tok_ t1))  )  (laB_1 q1_T2_S21 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S23 t2) (and (not (tok_ t2)) (g_ t2)) (is_active_1 false ?sch0 (sends_ t2)))  (laB_1 q1_accept_S34 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S23 t2)  )  (laB_1 q1_T1_S23 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S23 t2)  (g_ t2)  (is_active_1 false ?sch0 (sends_ t2)))  (laB_1 q1_T1_S35 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S23 t2)  (not (tok_ t2))  )  (laB_1 q1_T2_S21 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S40 t0) (and (tok_ t0) (not (g_ t0))) )  (laB_1 q1_T4_S8 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S40 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T0_S17 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S40 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T0_S8 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S40 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T4_S8 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S40 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T1_S17 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S40 t0) (and (tok_ t0) (not (g_ t0))) )  (laB_1 q1_T0_S8 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S40 t1) (and (tok_ t1) (not (g_ t1))) )  (laB_1 q1_T4_S8 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S40 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T0_S17 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S40 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T0_S8 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S40 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T4_S8 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S40 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T1_S17 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S40 t1) (and (tok_ t1) (not (g_ t1))) )  (laB_1 q1_T0_S8 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S40 t2) (and (tok_ t2) (not (g_ t2))) )  (laB_1 q1_T4_S8 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S40 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T0_S17 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S40 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T0_S8 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S40 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T4_S8 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S40 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T1_S17 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S40 t2) (and (tok_ t2) (not (g_ t2))) )  (laB_1 q1_T0_S8 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S29 t0) (and (not (tok_ t0)) (not (g_ t0))) (is_active_1 false true (sends_ t0)))  (laB_1 q1_T0_S25 (tau_sch_1 t0 true false true (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t0)  (not (tok_ t0))  )  (laB_1 q1_T1_S31 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t0)  (not (tok_ t0))  )  (laB_1 q1_T3_S29 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_S29 t0) (and (not (tok_ t0)) (not (g_ t0))) (is_active_1 false true (sends_ t0)))  (laB_1 q1_T0_S27 (tau_sch_1 t0 true false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S29 t0) (and (not (tok_ t0)) (not (g_ t0))) (is_active_1 false false (sends_ t0)))  (laB_1 q1_T1_S27 (tau_sch_1 t0 true false false (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t0)  (not (tok_ t0))  )  (laB_1 q1_T0_S29 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t0)  (not (tok_ t0))  )  (laB_1 q1_T0_S31 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_S29 t0) (and (not (tok_ t0)) (not (g_ t0))) (is_active_1 false false (sends_ t0)))  (laB_1 q1_accept_S25 (tau_sch_1 t0 true false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S29 t0) (and (tok_ t0) (not (g_ t0))) (is_active_1 false true (sends_ t0)))  (laB_1 q1_T0_S25 (tau_sch_1 t0 true false true (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t0)  (tok_ t0)  )  (laB_1 q1_T3_S29 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t0)  (tok_ t0)  )  (laB_1 q1_T0_S29 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_S29 t0) (and (tok_ t0) (not (g_ t0))) (is_active_1 false false (sends_ t0)))  (laB_1 q1_accept_S25 (tau_sch_1 t0 true false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S29 t1) (and (not (tok_ t1)) (not (g_ t1))) (is_active_1 false true (sends_ t1)))  (laB_1 q1_T0_S25 (tau_sch_1 t1 true false true (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t1)  (not (tok_ t1))  )  (laB_1 q1_T1_S31 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t1)  (not (tok_ t1))  )  (laB_1 q1_T3_S29 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_S29 t1) (and (not (tok_ t1)) (not (g_ t1))) (is_active_1 false true (sends_ t1)))  (laB_1 q1_T0_S27 (tau_sch_1 t1 true false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S29 t1) (and (not (tok_ t1)) (not (g_ t1))) (is_active_1 false false (sends_ t1)))  (laB_1 q1_T1_S27 (tau_sch_1 t1 true false false (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t1)  (not (tok_ t1))  )  (laB_1 q1_T0_S29 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t1)  (not (tok_ t1))  )  (laB_1 q1_T0_S31 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_S29 t1) (and (not (tok_ t1)) (not (g_ t1))) (is_active_1 false false (sends_ t1)))  (laB_1 q1_accept_S25 (tau_sch_1 t1 true false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S29 t1) (and (tok_ t1) (not (g_ t1))) (is_active_1 false true (sends_ t1)))  (laB_1 q1_T0_S25 (tau_sch_1 t1 true false true (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t1)  (tok_ t1)  )  (laB_1 q1_T3_S29 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t1)  (tok_ t1)  )  (laB_1 q1_T0_S29 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_S29 t1) (and (tok_ t1) (not (g_ t1))) (is_active_1 false false (sends_ t1)))  (laB_1 q1_accept_S25 (tau_sch_1 t1 true false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S29 t2) (and (not (tok_ t2)) (not (g_ t2))) (is_active_1 false true (sends_ t2)))  (laB_1 q1_T0_S25 (tau_sch_1 t2 true false true (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t2)  (not (tok_ t2))  )  (laB_1 q1_T1_S31 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t2)  (not (tok_ t2))  )  (laB_1 q1_T3_S29 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S29 t2) (and (not (tok_ t2)) (not (g_ t2))) (is_active_1 false true (sends_ t2)))  (laB_1 q1_T0_S27 (tau_sch_1 t2 true false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S29 t2) (and (not (tok_ t2)) (not (g_ t2))) (is_active_1 false false (sends_ t2)))  (laB_1 q1_T1_S27 (tau_sch_1 t2 true false false (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t2)  (not (tok_ t2))  )  (laB_1 q1_T0_S29 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t2)  (not (tok_ t2))  )  (laB_1 q1_T0_S31 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S29 t2) (and (not (tok_ t2)) (not (g_ t2))) (is_active_1 false false (sends_ t2)))  (laB_1 q1_accept_S25 (tau_sch_1 t2 true false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S29 t2) (and (tok_ t2) (not (g_ t2))) (is_active_1 false true (sends_ t2)))  (laB_1 q1_T0_S25 (tau_sch_1 t2 true false true (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t2)  (tok_ t2)  )  (laB_1 q1_T3_S29 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S29 t2)  (tok_ t2)  )  (laB_1 q1_T0_S29 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S29 t2) (and (tok_ t2) (not (g_ t2))) (is_active_1 false false (sends_ t2)))  (laB_1 q1_accept_S25 (tau_sch_1 t2 true false false (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t0)  (not (tok_ t0))  )  (and (laB_1 q1_T1_S16 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (>= (laC_1 q1_T1_S16 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S7 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t0)  (not (tok_ t0))  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S7 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S7 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t0)  (not (tok_ t0))  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S7 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t0)  (not (tok_ t0))  )  (and (laB_1 q1_T0_S16 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S16 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S7 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t0)  (tok_ t0)  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S7 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S7 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t0)  (tok_ t0)  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S7 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t1)  (not (tok_ t1))  )  (and (laB_1 q1_T1_S16 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (>= (laC_1 q1_T1_S16 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S7 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t1)  (not (tok_ t1))  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S7 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S7 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t1)  (not (tok_ t1))  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S7 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t1)  (not (tok_ t1))  )  (and (laB_1 q1_T0_S16 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S16 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S7 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t1)  (tok_ t1)  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S7 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S7 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t1)  (tok_ t1)  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S7 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t2)  (not (tok_ t2))  )  (and (laB_1 q1_T1_S16 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (>= (laC_1 q1_T1_S16 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S7 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t2)  (not (tok_ t2))  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S7 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S7 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t2)  (not (tok_ t2))  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S7 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t2)  (not (tok_ t2))  )  (and (laB_1 q1_T0_S16 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S16 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S7 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t2)  (tok_ t2)  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S7 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S7 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S7 t2)  (tok_ t2)  )  (and (laB_1 q1_T0_S7 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S7 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S7 t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S16 t0)  )  (and (laB_1 q1_T1_S16 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) (>= (laC_1 q1_T1_S16 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) (laC_1 q1_T1_S16 t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S16 t0)  (not (tok_ t0))  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) (> (laC_1 q1_accept_S7 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) (laC_1 q1_T1_S16 t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S16 t1)  )  (and (laB_1 q1_T1_S16 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) (>= (laC_1 q1_T1_S16 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) (laC_1 q1_T1_S16 t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S16 t1)  (not (tok_ t1))  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) (> (laC_1 q1_accept_S7 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) (laC_1 q1_T1_S16 t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S16 t2)  )  (and (laB_1 q1_T1_S16 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) (>= (laC_1 q1_T1_S16 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) (laC_1 q1_T1_S16 t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S16 t2)  (not (tok_ t2))  )  (and (laB_1 q1_accept_S7 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) (> (laC_1 q1_accept_S7 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) (laC_1 q1_T1_S16 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S23 t0)  (not (tok_ t0))  )  (laB_1 q1_T2_S21 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S23 t0)  (not (tok_ t0))  )  (laB_1 q1_T0_S21 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_S23 t0)  (g_ t0)  (is_active_1 false false (sends_ t0)))  (laB_1 q1_T1_S35 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S23 t0) (and (not (tok_ t0)) (g_ t0)) (is_active_1 false true (sends_ t0)))  (laB_1 q1_T0_S34 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S23 t0)  )  (laB_1 q1_T0_S23 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_S23 t0)  (g_ t0)  (is_active_1 false true (sends_ t0)))  (laB_1 q1_T0_S35 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S23 t0)  )  (laB_1 q1_T1_S23 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_S23 t0) (and (not (tok_ t0)) (g_ t0)) (is_active_1 false false (sends_ t0)))  (laB_1 q1_accept_S34 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S23 t1)  (not (tok_ t1))  )  (laB_1 q1_T2_S21 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S23 t1)  (not (tok_ t1))  )  (laB_1 q1_T0_S21 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_S23 t1)  (g_ t1)  (is_active_1 false false (sends_ t1)))  (laB_1 q1_T1_S35 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S23 t1) (and (not (tok_ t1)) (g_ t1)) (is_active_1 false true (sends_ t1)))  (laB_1 q1_T0_S34 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S23 t1)  )  (laB_1 q1_T0_S23 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_S23 t1)  (g_ t1)  (is_active_1 false true (sends_ t1)))  (laB_1 q1_T0_S35 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S23 t1)  )  (laB_1 q1_T1_S23 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_S23 t1) (and (not (tok_ t1)) (g_ t1)) (is_active_1 false false (sends_ t1)))  (laB_1 q1_accept_S34 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S23 t2)  (not (tok_ t2))  )  (laB_1 q1_T2_S21 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S23 t2)  (not (tok_ t2))  )  (laB_1 q1_T0_S21 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S23 t2)  (g_ t2)  (is_active_1 false false (sends_ t2)))  (laB_1 q1_T1_S35 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S23 t2) (and (not (tok_ t2)) (g_ t2)) (is_active_1 false true (sends_ t2)))  (laB_1 q1_T0_S34 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S23 t2)  )  (laB_1 q1_T0_S23 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S23 t2)  (g_ t2)  (is_active_1 false true (sends_ t2)))  (laB_1 q1_T0_S35 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S23 t2)  )  (laB_1 q1_T1_S23 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S23 t2) (and (not (tok_ t2)) (g_ t2)) (is_active_1 false false (sends_ t2)))  (laB_1 q1_accept_S34 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S23 t0) (and (not (tok_ t0)) (g_ t0)) (is_active_1 false ?sch0 (sends_ t0)))  (laB_1 q1_accept_S34 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S23 t0)  )  (laB_1 q1_T2_S23 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S23 t0)  (g_ t0)  (is_active_1 false ?sch0 (sends_ t0)))  (laB_1 q1_T0_S35 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S23 t0)  (not (tok_ t0))  )  (laB_1 q1_T2_S21 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S23 t1) (and (not (tok_ t1)) (g_ t1)) (is_active_1 false ?sch0 (sends_ t1)))  (laB_1 q1_accept_S34 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S23 t1)  )  (laB_1 q1_T2_S23 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S23 t1)  (g_ t1)  (is_active_1 false ?sch0 (sends_ t1)))  (laB_1 q1_T0_S35 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S23 t1)  (not (tok_ t1))  )  (laB_1 q1_T2_S21 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S23 t2) (and (not (tok_ t2)) (g_ t2)) (is_active_1 false ?sch0 (sends_ t2)))  (laB_1 q1_accept_S34 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S23 t2)  )  (laB_1 q1_T2_S23 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S23 t2)  (g_ t2)  (is_active_1 false ?sch0 (sends_ t2)))  (laB_1 q1_T0_S35 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S23 t2)  (not (tok_ t2))  )  (laB_1 q1_T2_S21 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S21 t0) (and (tok_ t0) (g_ t0)) (is_active_1 false ?sch0 (sends_ t0)))  (laB_1 q1_accept_S34 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S21 t0)  (tok_ t0)  )  (laB_1 q1_T2_S21 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S21 t0)  (not (tok_ t0))  )  (laB_1 q1_T2_S23 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S21 t0) (and (not (tok_ t0)) (g_ t0)) (is_active_1 false ?sch0 (sends_ t0)))  (laB_1 q1_accept_S34 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S21 t0)  (not (tok_ t0))  )  (laB_1 q1_T2_S21 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S21 t0) (and (not (tok_ t0)) (g_ t0)) (is_active_1 false ?sch0 (sends_ t0)))  (laB_1 q1_T0_S35 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S21 t1) (and (tok_ t1) (g_ t1)) (is_active_1 false ?sch0 (sends_ t1)))  (laB_1 q1_accept_S34 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S21 t1)  (tok_ t1)  )  (laB_1 q1_T2_S21 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S21 t1)  (not (tok_ t1))  )  (laB_1 q1_T2_S23 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S21 t1) (and (not (tok_ t1)) (g_ t1)) (is_active_1 false ?sch0 (sends_ t1)))  (laB_1 q1_accept_S34 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S21 t1)  (not (tok_ t1))  )  (laB_1 q1_T2_S21 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S21 t1) (and (not (tok_ t1)) (g_ t1)) (is_active_1 false ?sch0 (sends_ t1)))  (laB_1 q1_T0_S35 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S21 t2) (and (tok_ t2) (g_ t2)) (is_active_1 false ?sch0 (sends_ t2)))  (laB_1 q1_accept_S34 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S21 t2)  (tok_ t2)  )  (laB_1 q1_T2_S21 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S21 t2)  (not (tok_ t2))  )  (laB_1 q1_T2_S23 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S21 t2) (and (not (tok_ t2)) (g_ t2)) (is_active_1 false ?sch0 (sends_ t2)))  (laB_1 q1_accept_S34 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T2_S21 t2)  (not (tok_ t2))  )  (laB_1 q1_T2_S21 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T2_S21 t2) (and (not (tok_ t2)) (g_ t2)) (is_active_1 false ?sch0 (sends_ t2)))  (laB_1 q1_T0_S35 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S18 t0)  (g_ t0)  )  (laB_1 q1_T1_S41 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S18 t0)  )  (laB_1 q1_T1_S18 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S18 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_T0_S40 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S18 t0)  (not (tok_ t0))  )  (laB_1 q1_T5_S9 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S18 t1)  (g_ t1)  )  (laB_1 q1_T1_S41 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S18 t1)  )  (laB_1 q1_T1_S18 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S18 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_T0_S40 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S18 t1)  (not (tok_ t1))  )  (laB_1 q1_T5_S9 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S18 t2)  (g_ t2)  )  (laB_1 q1_T1_S41 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S18 t2)  )  (laB_1 q1_T1_S18 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S18 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_T0_S40 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S18 t2)  (not (tok_ t2))  )  (laB_1 q1_T5_S9 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S31 t0) (and (not (tok_ t0)) (not (g_ t0))) (is_active_1 false ?sch0 (sends_ t0)))  (laB_1 q1_accept_S25 (tau_sch_1 t0 true false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S31 t0)  )  (laB_1 q1_T3_S31 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S31 t0)  (not (g_ t0))  (is_active_1 false ?sch0 (sends_ t0)))  (laB_1 q1_T0_S27 (tau_sch_1 t0 true false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S31 t0)  (not (tok_ t0))  )  (laB_1 q1_T3_S29 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S31 t1) (and (not (tok_ t1)) (not (g_ t1))) (is_active_1 false ?sch0 (sends_ t1)))  (laB_1 q1_accept_S25 (tau_sch_1 t1 true false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S31 t1)  )  (laB_1 q1_T3_S31 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S31 t1)  (not (g_ t1))  (is_active_1 false ?sch0 (sends_ t1)))  (laB_1 q1_T0_S27 (tau_sch_1 t1 true false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S31 t1)  (not (tok_ t1))  )  (laB_1 q1_T3_S29 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S31 t2) (and (not (tok_ t2)) (not (g_ t2))) (is_active_1 false ?sch0 (sends_ t2)))  (laB_1 q1_accept_S25 (tau_sch_1 t2 true false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S31 t2)  )  (laB_1 q1_T3_S31 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T3_S31 t2)  (not (g_ t2))  (is_active_1 false ?sch0 (sends_ t2)))  (laB_1 q1_T0_S27 (tau_sch_1 t2 true false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T3_S31 t2)  (not (tok_ t2))  )  (laB_1 q1_T3_S29 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S11 t0)  (not (tok_ t0))  )  (laB_1 q1_T6_S19 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S11 t0) (and (not (sends_ t0)) (tok_ t0)) )  (laB_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S11 t0)  (not (tok_ t0))  )  (laB_1 q1_T6_S11 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S11 t0)  (tok_ t0)  )  (laB_1 q1_T6_S11 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S11 t1)  (not (tok_ t1))  )  (laB_1 q1_T6_S19 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S11 t1) (and (not (sends_ t1)) (tok_ t1)) )  (laB_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S11 t1)  (not (tok_ t1))  )  (laB_1 q1_T6_S11 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S11 t1)  (tok_ t1)  )  (laB_1 q1_T6_S11 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S11 t2)  (not (tok_ t2))  )  (laB_1 q1_T6_S19 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S11 t2) (and (not (sends_ t2)) (tok_ t2)) )  (laB_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S11 t2)  (not (tok_ t2))  )  (laB_1 q1_T6_S11 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T6_S11 t2)  (tok_ t2)  )  (laB_1 q1_T6_S11 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S21 t0) (and (tok_ t0) (g_ t0)) (is_active_1 false true (sends_ t0)))  (laB_1 q1_T0_S34 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t0)  (not (tok_ t0))  )  (laB_1 q1_T1_S23 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t0)  (not (tok_ t0))  )  (laB_1 q1_T2_S21 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t0)  (not (tok_ t0))  )  (laB_1 q1_T0_S21 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t0)  (not (tok_ t0))  )  (laB_1 q1_T0_S23 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_S21 t0) (and (tok_ t0) (g_ t0)) (is_active_1 false false (sends_ t0)))  (laB_1 q1_accept_S34 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S21 t0) (and (not (tok_ t0)) (g_ t0)) (is_active_1 false true (sends_ t0)))  (laB_1 q1_T0_S34 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t0)  (tok_ t0)  )  (laB_1 q1_T2_S21 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_S21 t0) (and (not (tok_ t0)) (g_ t0)) (is_active_1 false true (sends_ t0)))  (laB_1 q1_T0_S35 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S21 t0) (and (not (tok_ t0)) (g_ t0)) (is_active_1 false false (sends_ t0)))  (laB_1 q1_T1_S35 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t0)  (tok_ t0)  )  (laB_1 q1_T0_S21 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_S21 t0) (and (not (tok_ t0)) (g_ t0)) (is_active_1 false false (sends_ t0)))  (laB_1 q1_accept_S34 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S21 t1) (and (tok_ t1) (g_ t1)) (is_active_1 false true (sends_ t1)))  (laB_1 q1_T0_S34 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t1)  (not (tok_ t1))  )  (laB_1 q1_T1_S23 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t1)  (not (tok_ t1))  )  (laB_1 q1_T2_S21 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t1)  (not (tok_ t1))  )  (laB_1 q1_T0_S21 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t1)  (not (tok_ t1))  )  (laB_1 q1_T0_S23 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_S21 t1) (and (tok_ t1) (g_ t1)) (is_active_1 false false (sends_ t1)))  (laB_1 q1_accept_S34 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S21 t1) (and (not (tok_ t1)) (g_ t1)) (is_active_1 false true (sends_ t1)))  (laB_1 q1_T0_S34 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t1)  (tok_ t1)  )  (laB_1 q1_T2_S21 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_S21 t1) (and (not (tok_ t1)) (g_ t1)) (is_active_1 false true (sends_ t1)))  (laB_1 q1_T0_S35 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S21 t1) (and (not (tok_ t1)) (g_ t1)) (is_active_1 false false (sends_ t1)))  (laB_1 q1_T1_S35 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t1)  (tok_ t1)  )  (laB_1 q1_T0_S21 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_S21 t1) (and (not (tok_ t1)) (g_ t1)) (is_active_1 false false (sends_ t1)))  (laB_1 q1_accept_S34 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S21 t2) (and (tok_ t2) (g_ t2)) (is_active_1 false true (sends_ t2)))  (laB_1 q1_T0_S34 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t2)  (not (tok_ t2))  )  (laB_1 q1_T1_S23 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t2)  (not (tok_ t2))  )  (laB_1 q1_T2_S21 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t2)  (not (tok_ t2))  )  (laB_1 q1_T0_S21 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t2)  (not (tok_ t2))  )  (laB_1 q1_T0_S23 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S21 t2) (and (tok_ t2) (g_ t2)) (is_active_1 false false (sends_ t2)))  (laB_1 q1_accept_S34 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S21 t2) (and (not (tok_ t2)) (g_ t2)) (is_active_1 false true (sends_ t2)))  (laB_1 q1_T0_S34 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t2)  (tok_ t2)  )  (laB_1 q1_T2_S21 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S21 t2) (and (not (tok_ t2)) (g_ t2)) (is_active_1 false true (sends_ t2)))  (laB_1 q1_T0_S35 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S21 t2) (and (not (tok_ t2)) (g_ t2)) (is_active_1 false false (sends_ t2)))  (laB_1 q1_T1_S35 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S21 t2)  (tok_ t2)  )  (laB_1 q1_T0_S21 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S21 t2) (and (not (tok_ t2)) (g_ t2)) (is_active_1 false false (sends_ t2)))  (laB_1 q1_accept_S34 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_T0_S40 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t0)  (not (tok_ t0))  )  (laB_1 q1_T1_S18 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t0)  (not (tok_ t0))  )  (laB_1 q1_T5_S9 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_accept_S41 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_T1_S41 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t0)  (not (tok_ t0))  )  (laB_1 q1_T0_S9 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t0)  (not (tok_ t0))  )  (laB_1 q1_T0_S18 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t0) (and (tok_ t0) (g_ t0)) )  (laB_1 q1_T0_S40 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t0)  (tok_ t0)  )  (laB_1 q1_T5_S9 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t0)  (tok_ t0)  )  (laB_1 q1_T0_S9 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_T0_S40 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t1)  (not (tok_ t1))  )  (laB_1 q1_T1_S18 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t1)  (not (tok_ t1))  )  (laB_1 q1_T5_S9 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_accept_S41 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_T1_S41 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t1)  (not (tok_ t1))  )  (laB_1 q1_T0_S9 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t1)  (not (tok_ t1))  )  (laB_1 q1_T0_S18 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t1) (and (tok_ t1) (g_ t1)) )  (laB_1 q1_T0_S40 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t1)  (tok_ t1)  )  (laB_1 q1_T5_S9 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t1)  (tok_ t1)  )  (laB_1 q1_T0_S9 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_T0_S40 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t2)  (not (tok_ t2))  )  (laB_1 q1_T1_S18 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t2)  (not (tok_ t2))  )  (laB_1 q1_T5_S9 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_accept_S41 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_T1_S41 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t2)  (not (tok_ t2))  )  (laB_1 q1_T0_S9 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t2)  (not (tok_ t2))  )  (laB_1 q1_T0_S18 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t2) (and (tok_ t2) (g_ t2)) )  (laB_1 q1_T0_S40 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t2)  (tok_ t2)  )  (laB_1 q1_T5_S9 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S9 t2)  (tok_ t2)  )  (laB_1 q1_T0_S9 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S27 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S25 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S27 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S27 t0)  (not (g_ t0))  )  (and (laB_1 q1_T0_S27 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S27 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S27 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S27 t0)  (not (g_ t0))  )  (and (laB_1 q1_T1_S27 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (>= (laC_1 q1_T1_S27 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S27 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S27 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S27 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S27 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S25 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S27 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S27 t1)  (not (g_ t1))  )  (and (laB_1 q1_T0_S27 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S27 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S27 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S27 t1)  (not (g_ t1))  )  (and (laB_1 q1_T1_S27 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (>= (laC_1 q1_T1_S27 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S27 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S27 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S27 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S27 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S25 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S27 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S27 t2)  (not (g_ t2))  )  (and (laB_1 q1_T0_S27 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S27 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S27 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S27 t2)  (not (g_ t2))  )  (and (laB_1 q1_T1_S27 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (>= (laC_1 q1_T1_S27 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S27 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S27 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S27 t2))) )))
(assert (=> (and (laB_1 q1_T0_S35 t0)  (g_ t0)  )  (and (laB_1 q1_T0_S35 (tau_sch_1 t0 false false true (sends_ t0))) (>= (laC_1 q1_T0_S35 (tau_sch_1 t0 false false true (sends_ t0))) (laC_1 q1_T0_S35 t0))) ))
(assert (=> (and (laB_1 q1_T0_S35 t0)  (g_ t0)  )  (and (laB_1 q1_T1_S35 (tau_sch_1 t0 false false false (sends_ t0))) (>= (laC_1 q1_T1_S35 (tau_sch_1 t0 false false false (sends_ t0))) (laC_1 q1_T0_S35 t0))) ))
(assert (=> (and (laB_1 q1_T0_S35 t0) (and (not (tok_ t0)) (g_ t0)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t0 false false true (sends_ t0))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t0 false false true (sends_ t0))) (laC_1 q1_T0_S35 t0))) ))
(assert (=> (and (laB_1 q1_T0_S35 t0) (and (not (tok_ t0)) (g_ t0)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t0 false false false (sends_ t0))) (> (laC_1 q1_accept_S34 (tau_sch_1 t0 false false false (sends_ t0))) (laC_1 q1_T0_S35 t0))) ))
(assert (=> (and (laB_1 q1_T0_S35 t1)  (g_ t1)  )  (and (laB_1 q1_T0_S35 (tau_sch_1 t1 false false true (sends_ t1))) (>= (laC_1 q1_T0_S35 (tau_sch_1 t1 false false true (sends_ t1))) (laC_1 q1_T0_S35 t1))) ))
(assert (=> (and (laB_1 q1_T0_S35 t1)  (g_ t1)  )  (and (laB_1 q1_T1_S35 (tau_sch_1 t1 false false false (sends_ t1))) (>= (laC_1 q1_T1_S35 (tau_sch_1 t1 false false false (sends_ t1))) (laC_1 q1_T0_S35 t1))) ))
(assert (=> (and (laB_1 q1_T0_S35 t1) (and (not (tok_ t1)) (g_ t1)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t1 false false true (sends_ t1))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t1 false false true (sends_ t1))) (laC_1 q1_T0_S35 t1))) ))
(assert (=> (and (laB_1 q1_T0_S35 t1) (and (not (tok_ t1)) (g_ t1)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t1 false false false (sends_ t1))) (> (laC_1 q1_accept_S34 (tau_sch_1 t1 false false false (sends_ t1))) (laC_1 q1_T0_S35 t1))) ))
(assert (=> (and (laB_1 q1_T0_S35 t2)  (g_ t2)  )  (and (laB_1 q1_T0_S35 (tau_sch_1 t2 false false true (sends_ t2))) (>= (laC_1 q1_T0_S35 (tau_sch_1 t2 false false true (sends_ t2))) (laC_1 q1_T0_S35 t2))) ))
(assert (=> (and (laB_1 q1_T0_S35 t2)  (g_ t2)  )  (and (laB_1 q1_T1_S35 (tau_sch_1 t2 false false false (sends_ t2))) (>= (laC_1 q1_T1_S35 (tau_sch_1 t2 false false false (sends_ t2))) (laC_1 q1_T0_S35 t2))) ))
(assert (=> (and (laB_1 q1_T0_S35 t2) (and (not (tok_ t2)) (g_ t2)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t2 false false true (sends_ t2))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t2 false false true (sends_ t2))) (laC_1 q1_T0_S35 t2))) ))
(assert (=> (and (laB_1 q1_T0_S35 t2) (and (not (tok_ t2)) (g_ t2)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t2 false false false (sends_ t2))) (> (laC_1 q1_accept_S34 (tau_sch_1 t2 false false false (sends_ t2))) (laC_1 q1_T0_S35 t2))) ))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S17 t0)  (not (g_ t0))  )  (laB_1 q1_T1_S17 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S17 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_accept_S7 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S17 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T4_S8 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S17 t0)  (g_ t0)  )  (laB_1 q1_T1_S16 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S17 t1)  (not (g_ t1))  )  (laB_1 q1_T1_S17 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S17 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_accept_S7 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S17 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T4_S8 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S17 t1)  (g_ t1)  )  (laB_1 q1_T1_S16 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S17 t2)  (not (g_ t2))  )  (laB_1 q1_T1_S17 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S17 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_accept_S7 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S17 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T4_S8 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S17 t2)  (g_ t2)  )  (laB_1 q1_T1_S16 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S17 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_T0_S7 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S17 t0)  (not (g_ t0))  )  (laB_1 q1_T1_S17 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S17 t0)  (g_ t0)  )  (laB_1 q1_T1_S16 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S17 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T0_S8 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S17 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T4_S8 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S17 t0)  (g_ t0)  )  (laB_1 q1_T0_S16 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S17 t0)  (not (g_ t0))  )  (laB_1 q1_T0_S17 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S17 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_accept_S7 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S17 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_T0_S7 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S17 t1)  (not (g_ t1))  )  (laB_1 q1_T1_S17 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S17 t1)  (g_ t1)  )  (laB_1 q1_T1_S16 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S17 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T0_S8 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S17 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T4_S8 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S17 t1)  (g_ t1)  )  (laB_1 q1_T0_S16 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S17 t1)  (not (g_ t1))  )  (laB_1 q1_T0_S17 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S17 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_accept_S7 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S17 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_T0_S7 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S17 t2)  (not (g_ t2))  )  (laB_1 q1_T1_S17 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S17 t2)  (g_ t2)  )  (laB_1 q1_T1_S16 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S17 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T0_S8 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S17 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T4_S8 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S17 t2)  (g_ t2)  )  (laB_1 q1_T0_S16 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S17 t2)  (not (g_ t2))  )  (laB_1 q1_T0_S17 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S17 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_accept_S7 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t0)  (not (tok_ t0))  )  (laB_1 q1_T1_S19 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t0)  (not (tok_ t0))  )  (laB_1 q1_T6_S11 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t0)  (not (tok_ t0))  )  (laB_1 q1_T0_S11 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t0)  (not (tok_ t0))  )  (laB_1 q1_T0_S19 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t0) (and (not (sends_ t0)) (tok_ t0)) )  (laB_1 q1_T0_S10 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t0)  (tok_ t0)  )  (laB_1 q1_T6_S11 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t0) (and (not (sends_ t0)) (tok_ t0)) )  (laB_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t0)  (tok_ t0)  )  (laB_1 q1_T0_S11 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t1)  (not (tok_ t1))  )  (laB_1 q1_T1_S19 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t1)  (not (tok_ t1))  )  (laB_1 q1_T6_S11 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t1)  (not (tok_ t1))  )  (laB_1 q1_T0_S11 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t1)  (not (tok_ t1))  )  (laB_1 q1_T0_S19 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t1) (and (not (sends_ t1)) (tok_ t1)) )  (laB_1 q1_T0_S10 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t1)  (tok_ t1)  )  (laB_1 q1_T6_S11 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t1) (and (not (sends_ t1)) (tok_ t1)) )  (laB_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t1)  (tok_ t1)  )  (laB_1 q1_T0_S11 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t2)  (not (tok_ t2))  )  (laB_1 q1_T1_S19 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t2)  (not (tok_ t2))  )  (laB_1 q1_T6_S11 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t2)  (not (tok_ t2))  )  (laB_1 q1_T0_S11 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t2)  (not (tok_ t2))  )  (laB_1 q1_T0_S19 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t2) (and (not (sends_ t2)) (tok_ t2)) )  (laB_1 q1_T0_S10 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t2)  (tok_ t2)  )  (laB_1 q1_T6_S11 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t2) (and (not (sends_ t2)) (tok_ t2)) )  (laB_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S11 t2)  (tok_ t2)  )  (laB_1 q1_T0_S11 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t0) (and (tok_ t0) (g_ t0)) )  (laB_1 q1_accept_S7 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t0) (and (tok_ t0) (not (g_ t0))) )  (laB_1 q1_T4_S8 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_accept_S7 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_T0_S16 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T4_S17 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T4_S8 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t1) (and (tok_ t1) (g_ t1)) )  (laB_1 q1_accept_S7 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t1) (and (tok_ t1) (not (g_ t1))) )  (laB_1 q1_T4_S8 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_accept_S7 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_T0_S16 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T4_S17 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T4_S8 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t2) (and (tok_ t2) (g_ t2)) )  (laB_1 q1_accept_S7 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t2) (and (tok_ t2) (not (g_ t2))) )  (laB_1 q1_T4_S8 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_accept_S7 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_T0_S16 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T4_S17 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S8 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T4_S8 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_S8 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_accept_S7 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S8 t0) (and (tok_ t0) (not (g_ t0))) )  (laB_1 q1_T4_S8 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S8 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_T0_S16 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S8 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_T0_S7 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S8 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T0_S17 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S8 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T0_S8 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S8 t0) (and (tok_ t0) (g_ t0)) )  (laB_1 q1_T0_S7 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S8 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T1_S17 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S8 t0) (and (tok_ t0) (g_ t0)) )  (laB_1 q1_accept_S7 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S8 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_T1_S16 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S8 t0) (and (tok_ t0) (not (g_ t0))) )  (laB_1 q1_T0_S8 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S8 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T4_S8 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_S8 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_accept_S7 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S8 t1) (and (tok_ t1) (not (g_ t1))) )  (laB_1 q1_T4_S8 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S8 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_T0_S16 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S8 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_T0_S7 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S8 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T0_S17 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S8 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T0_S8 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S8 t1) (and (tok_ t1) (g_ t1)) )  (laB_1 q1_T0_S7 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S8 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T1_S17 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S8 t1) (and (tok_ t1) (g_ t1)) )  (laB_1 q1_accept_S7 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S8 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_T1_S16 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S8 t1) (and (tok_ t1) (not (g_ t1))) )  (laB_1 q1_T0_S8 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S8 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T4_S8 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_S8 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_accept_S7 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S8 t2) (and (tok_ t2) (not (g_ t2))) )  (laB_1 q1_T4_S8 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S8 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_T0_S16 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S8 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_T0_S7 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S8 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T0_S17 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S8 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T0_S8 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S8 t2) (and (tok_ t2) (g_ t2)) )  (laB_1 q1_T0_S7 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S8 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T1_S17 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S8 t2) (and (tok_ t2) (g_ t2)) )  (laB_1 q1_accept_S7 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S8 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_T1_S16 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S8 t2) (and (tok_ t2) (not (g_ t2))) )  (laB_1 q1_T0_S8 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_S8 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T4_S8 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_T0_S7 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_init t0) (and (tok_ t0) (not (g_ t0))) )  (laB_1 q1_T4_S8 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_T0_S16 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T0_S17 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (not (g_ t0))) (is_active_1 false false (sends_ t0)))  (laB_1 q1_accept_S25 (tau_sch_1 t0 true false false (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t0) (and (tok_ t0) (g_ t0)) )  (laB_1 q1_T0_S7 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T1_S17 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t0) (and (not (sends_ t0)) (tok_ t0) (not (g_ t0))) )  (laB_1 q1_T0_S10 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t0) (and (tok_ t0) (not (g_ t0))) ) (and (laB_1 q1_T6_S11 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laB_1 q1_T2_S21 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laB_1 q1_T3_S29 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laB_1 q1_T5_S9 (tau_sch_1 t0 ?r0 false false (sends_ t0)))))))
(assert (=> (and (laB_1 q1_T0_init t0) (and (tok_ t0) (not (g_ t0))) (is_active_1 false true (sends_ t0)))  (laB_1 q1_T0_S25 (tau_sch_1 t0 true false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (not (g_ t0))) (is_active_1 false true (sends_ t0)))  (laB_1 q1_T0_S27 (tau_sch_1 t0 true false true (sends_ t0))) ))
(assert (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T0_S8 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t0) (and (not (sends_ t0)) (tok_ t0) (not (g_ t0))) )  (laB_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_init t0) (and (tok_ t0) (not (g_ t0))) (is_active_1 false false (sends_ t0)))  (laB_1 q1_accept_S25 (tau_sch_1 t0 true false false (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t0) (and (tok_ t0) (g_ t0)) )  (laB_1 q1_accept_S7 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (not (g_ t0))) (is_active_1 false false (sends_ t0)))  (laB_1 q1_T1_S27 (tau_sch_1 t0 true false false (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t0) (and (tok_ t0) (not (g_ t0))) ) (and (laB_1 q1_T0_S29 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laB_1 q1_T0_S21 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laB_1 q1_T0_S9 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laB_1 q1_T0_S11 (tau_sch_1 t0 ?r0 false true (sends_ t0)))))))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (not (g_ t0))) ) (and (laB_1 q1_T0_S19 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laB_1 q1_T0_S31 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laB_1 q1_T0_S18 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laB_1 q1_T0_S23 (tau_sch_1 t0 ?r0 false true (sends_ t0)))))))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (not (g_ t0))) ) (and (laB_1 q1_T0_S29 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laB_1 q1_T0_S21 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laB_1 q1_T0_S9 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laB_1 q1_T0_S11 (tau_sch_1 t0 ?r0 false true (sends_ t0)))))))
(assert (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (not (g_ t0))) (is_active_1 false true (sends_ t0)))  (laB_1 q1_T0_S25 (tau_sch_1 t0 true false true (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_T1_S16 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_accept_S7 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (not (g_ t0))) ) (and (laB_1 q1_T6_S11 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laB_1 q1_T2_S21 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laB_1 q1_T3_S29 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laB_1 q1_T5_S9 (tau_sch_1 t0 ?r0 false false (sends_ t0)))))))
(assert (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T4_S8 (tau_sch_1 t0 false false false (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t0) (and (not (tok_ t0)) (not (g_ t0))) ) (and (laB_1 q1_T1_S19 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laB_1 q1_T1_S31 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laB_1 q1_T1_S23 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laB_1 q1_T1_S18 (tau_sch_1 t0 ?r0 false false (sends_ t0)))))))
(assert (=> (and (laB_1 q1_T0_init t0) (and (tok_ t0) (not (g_ t0))) )  (laB_1 q1_T0_S8 (tau_sch_1 t0 false false true (sends_ t0))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_T0_S7 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_init t1) (and (tok_ t1) (not (g_ t1))) )  (laB_1 q1_T4_S8 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_T0_S16 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T0_S17 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (not (g_ t1))) (is_active_1 false false (sends_ t1)))  (laB_1 q1_accept_S25 (tau_sch_1 t1 true false false (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t1) (and (tok_ t1) (g_ t1)) )  (laB_1 q1_T0_S7 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T1_S17 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t1) (and (not (sends_ t1)) (tok_ t1) (not (g_ t1))) )  (laB_1 q1_T0_S10 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t1) (and (tok_ t1) (not (g_ t1))) ) (and (laB_1 q1_T6_S11 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laB_1 q1_T2_S21 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laB_1 q1_T3_S29 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laB_1 q1_T5_S9 (tau_sch_1 t1 ?r0 false false (sends_ t1)))))))
(assert (=> (and (laB_1 q1_T0_init t1) (and (tok_ t1) (not (g_ t1))) (is_active_1 false true (sends_ t1)))  (laB_1 q1_T0_S25 (tau_sch_1 t1 true false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (not (g_ t1))) (is_active_1 false true (sends_ t1)))  (laB_1 q1_T0_S27 (tau_sch_1 t1 true false true (sends_ t1))) ))
(assert (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T0_S8 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t1) (and (not (sends_ t1)) (tok_ t1) (not (g_ t1))) )  (laB_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_init t1) (and (tok_ t1) (not (g_ t1))) (is_active_1 false false (sends_ t1)))  (laB_1 q1_accept_S25 (tau_sch_1 t1 true false false (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t1) (and (tok_ t1) (g_ t1)) )  (laB_1 q1_accept_S7 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (not (g_ t1))) (is_active_1 false false (sends_ t1)))  (laB_1 q1_T1_S27 (tau_sch_1 t1 true false false (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t1) (and (tok_ t1) (not (g_ t1))) ) (and (laB_1 q1_T0_S29 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laB_1 q1_T0_S21 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laB_1 q1_T0_S9 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laB_1 q1_T0_S11 (tau_sch_1 t1 ?r0 false true (sends_ t1)))))))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (not (g_ t1))) ) (and (laB_1 q1_T0_S19 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laB_1 q1_T0_S31 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laB_1 q1_T0_S18 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laB_1 q1_T0_S23 (tau_sch_1 t1 ?r0 false true (sends_ t1)))))))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (not (g_ t1))) ) (and (laB_1 q1_T0_S29 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laB_1 q1_T0_S21 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laB_1 q1_T0_S9 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laB_1 q1_T0_S11 (tau_sch_1 t1 ?r0 false true (sends_ t1)))))))
(assert (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (not (g_ t1))) (is_active_1 false true (sends_ t1)))  (laB_1 q1_T0_S25 (tau_sch_1 t1 true false true (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_T1_S16 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_accept_S7 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (not (g_ t1))) ) (and (laB_1 q1_T6_S11 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laB_1 q1_T2_S21 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laB_1 q1_T3_S29 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laB_1 q1_T5_S9 (tau_sch_1 t1 ?r0 false false (sends_ t1)))))))
(assert (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T4_S8 (tau_sch_1 t1 false false false (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t1) (and (not (tok_ t1)) (not (g_ t1))) ) (and (laB_1 q1_T1_S19 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laB_1 q1_T1_S31 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laB_1 q1_T1_S23 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laB_1 q1_T1_S18 (tau_sch_1 t1 ?r0 false false (sends_ t1)))))))
(assert (=> (and (laB_1 q1_T0_init t1) (and (tok_ t1) (not (g_ t1))) )  (laB_1 q1_T0_S8 (tau_sch_1 t1 false false true (sends_ t1))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_T0_S7 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_init t2) (and (tok_ t2) (not (g_ t2))) )  (laB_1 q1_T4_S8 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_T0_S16 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T0_S17 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (not (g_ t2))) (is_active_1 false false (sends_ t2)))  (laB_1 q1_accept_S25 (tau_sch_1 t2 true false false (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t2) (and (tok_ t2) (g_ t2)) )  (laB_1 q1_T0_S7 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T1_S17 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t2) (and (not (sends_ t2)) (tok_ t2) (not (g_ t2))) )  (laB_1 q1_T0_S10 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t2) (and (tok_ t2) (not (g_ t2))) ) (and (laB_1 q1_T6_S11 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laB_1 q1_T2_S21 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laB_1 q1_T3_S29 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laB_1 q1_T5_S9 (tau_sch_1 t2 ?r0 false false (sends_ t2)))))))
(assert (=> (and (laB_1 q1_T0_init t2) (and (tok_ t2) (not (g_ t2))) (is_active_1 false true (sends_ t2)))  (laB_1 q1_T0_S25 (tau_sch_1 t2 true false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (not (g_ t2))) (is_active_1 false true (sends_ t2)))  (laB_1 q1_T0_S27 (tau_sch_1 t2 true false true (sends_ t2))) ))
(assert (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T0_S8 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t2) (and (not (sends_ t2)) (tok_ t2) (not (g_ t2))) )  (laB_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_init t2) (and (tok_ t2) (not (g_ t2))) (is_active_1 false false (sends_ t2)))  (laB_1 q1_accept_S25 (tau_sch_1 t2 true false false (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t2) (and (tok_ t2) (g_ t2)) )  (laB_1 q1_accept_S7 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (not (g_ t2))) (is_active_1 false false (sends_ t2)))  (laB_1 q1_T1_S27 (tau_sch_1 t2 true false false (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t2) (and (tok_ t2) (not (g_ t2))) ) (and (laB_1 q1_T0_S29 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laB_1 q1_T0_S21 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laB_1 q1_T0_S9 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laB_1 q1_T0_S11 (tau_sch_1 t2 ?r0 false true (sends_ t2)))))))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (not (g_ t2))) ) (and (laB_1 q1_T0_S19 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laB_1 q1_T0_S31 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laB_1 q1_T0_S18 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laB_1 q1_T0_S23 (tau_sch_1 t2 ?r0 false true (sends_ t2)))))))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (not (g_ t2))) ) (and (laB_1 q1_T0_S29 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laB_1 q1_T0_S21 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laB_1 q1_T0_S9 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laB_1 q1_T0_S11 (tau_sch_1 t2 ?r0 false true (sends_ t2)))))))
(assert (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (not (g_ t2))) (is_active_1 false true (sends_ t2)))  (laB_1 q1_T0_S25 (tau_sch_1 t2 true false true (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_T1_S16 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_accept_S7 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (not (g_ t2))) ) (and (laB_1 q1_T6_S11 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laB_1 q1_T2_S21 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laB_1 q1_T3_S29 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laB_1 q1_T5_S9 (tau_sch_1 t2 ?r0 false false (sends_ t2)))))))
(assert (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T4_S8 (tau_sch_1 t2 false false false (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_init t2) (and (not (tok_ t2)) (not (g_ t2))) ) (and (laB_1 q1_T1_S19 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laB_1 q1_T1_S31 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laB_1 q1_T1_S23 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laB_1 q1_T1_S18 (tau_sch_1 t2 ?r0 false false (sends_ t2)))))))
(assert (=> (and (laB_1 q1_T0_init t2) (and (tok_ t2) (not (g_ t2))) )  (laB_1 q1_T0_S8 (tau_sch_1 t2 false false true (sends_ t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S37 t0)  (not (sends_ t0))  )  (and (laB_1 q1_T1_S37 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (>= (laC_1 q1_T1_S37 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S37 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S37 t0) (and (not (sends_ t0)) (not (tok_ t0))) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S37 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S37 t0) (and (not (sends_ t0)) (not (tok_ t0))) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S37 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S37 t0)  (not (sends_ t0))  )  (and (laB_1 q1_T0_S37 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S37 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S37 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S37 t1)  (not (sends_ t1))  )  (and (laB_1 q1_T1_S37 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (>= (laC_1 q1_T1_S37 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S37 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S37 t1) (and (not (sends_ t1)) (not (tok_ t1))) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S37 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S37 t1) (and (not (sends_ t1)) (not (tok_ t1))) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S37 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S37 t1)  (not (sends_ t1))  )  (and (laB_1 q1_T0_S37 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S37 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S37 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S37 t2)  (not (sends_ t2))  )  (and (laB_1 q1_T1_S37 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (>= (laC_1 q1_T1_S37 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S37 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S37 t2) (and (not (sends_ t2)) (not (tok_ t2))) )  (and (laB_1 q1_T0_S10 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S10 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S37 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S37 t2) (and (not (sends_ t2)) (not (tok_ t2))) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S37 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S37 t2)  (not (sends_ t2))  )  (and (laB_1 q1_T0_S37 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S37 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S37 t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S35 t0) (and (not (tok_ t0)) (g_ t0)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) (> (laC_1 q1_accept_S34 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) (laC_1 q1_T1_S35 t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S35 t0)  (g_ t0)  )  (and (laB_1 q1_T1_S35 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) (>= (laC_1 q1_T1_S35 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) (laC_1 q1_T1_S35 t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S35 t1) (and (not (tok_ t1)) (g_ t1)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) (> (laC_1 q1_accept_S34 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) (laC_1 q1_T1_S35 t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S35 t1)  (g_ t1)  )  (and (laB_1 q1_T1_S35 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) (>= (laC_1 q1_T1_S35 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) (laC_1 q1_T1_S35 t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S35 t2) (and (not (tok_ t2)) (g_ t2)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) (> (laC_1 q1_accept_S34 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) (laC_1 q1_T1_S35 t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T1_S35 t2)  (g_ t2)  )  (and (laB_1 q1_T1_S35 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) (>= (laC_1 q1_T1_S35 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) (laC_1 q1_T1_S35 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t0) (and (tok_ t0) (not (g_ t0))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S25 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_accept_S25 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t0) (and (tok_ t0) (not (g_ t0))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_accept_S25 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S25 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_accept_S25 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (and (laB_1 q1_T1_S27 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (>= (laC_1 q1_T1_S27 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_accept_S25 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (and (laB_1 q1_T0_S27 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S27 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_accept_S25 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_accept_S25 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t1) (and (tok_ t1) (not (g_ t1))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S25 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_accept_S25 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t1) (and (tok_ t1) (not (g_ t1))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_accept_S25 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S25 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_accept_S25 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (and (laB_1 q1_T1_S27 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (>= (laC_1 q1_T1_S27 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_accept_S25 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (and (laB_1 q1_T0_S27 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S27 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_accept_S25 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_accept_S25 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t2) (and (tok_ t2) (not (g_ t2))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S25 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_accept_S25 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t2) (and (tok_ t2) (not (g_ t2))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_accept_S25 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S25 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_accept_S25 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (and (laB_1 q1_T1_S27 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (>= (laC_1 q1_T1_S27 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_accept_S25 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (and (laB_1 q1_T0_S27 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S27 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_accept_S25 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_accept_S25 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_accept_S25 t2))) )))
(assert (=> (and (laB_1 q1_T0_S34 t0) (and (not (tok_ t0)) (g_ t0)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t0 false false true (sends_ t0))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t0 false false true (sends_ t0))) (laC_1 q1_T0_S34 t0))) ))
(assert (=> (and (laB_1 q1_T0_S34 t0) (and (not (tok_ t0)) (g_ t0)) )  (and (laB_1 q1_T0_S35 (tau_sch_1 t0 false false true (sends_ t0))) (>= (laC_1 q1_T0_S35 (tau_sch_1 t0 false false true (sends_ t0))) (laC_1 q1_T0_S34 t0))) ))
(assert (=> (and (laB_1 q1_T0_S34 t0) (and (tok_ t0) (g_ t0)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t0 false false false (sends_ t0))) (> (laC_1 q1_accept_S34 (tau_sch_1 t0 false false false (sends_ t0))) (laC_1 q1_T0_S34 t0))) ))
(assert (=> (and (laB_1 q1_T0_S34 t0) (and (tok_ t0) (g_ t0)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t0 false false true (sends_ t0))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t0 false false true (sends_ t0))) (laC_1 q1_T0_S34 t0))) ))
(assert (=> (and (laB_1 q1_T0_S34 t0) (and (not (tok_ t0)) (g_ t0)) )  (and (laB_1 q1_T1_S35 (tau_sch_1 t0 false false false (sends_ t0))) (>= (laC_1 q1_T1_S35 (tau_sch_1 t0 false false false (sends_ t0))) (laC_1 q1_T0_S34 t0))) ))
(assert (=> (and (laB_1 q1_T0_S34 t0) (and (not (tok_ t0)) (g_ t0)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t0 false false false (sends_ t0))) (> (laC_1 q1_accept_S34 (tau_sch_1 t0 false false false (sends_ t0))) (laC_1 q1_T0_S34 t0))) ))
(assert (=> (and (laB_1 q1_T0_S34 t1) (and (not (tok_ t1)) (g_ t1)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t1 false false true (sends_ t1))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t1 false false true (sends_ t1))) (laC_1 q1_T0_S34 t1))) ))
(assert (=> (and (laB_1 q1_T0_S34 t1) (and (not (tok_ t1)) (g_ t1)) )  (and (laB_1 q1_T0_S35 (tau_sch_1 t1 false false true (sends_ t1))) (>= (laC_1 q1_T0_S35 (tau_sch_1 t1 false false true (sends_ t1))) (laC_1 q1_T0_S34 t1))) ))
(assert (=> (and (laB_1 q1_T0_S34 t1) (and (tok_ t1) (g_ t1)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t1 false false false (sends_ t1))) (> (laC_1 q1_accept_S34 (tau_sch_1 t1 false false false (sends_ t1))) (laC_1 q1_T0_S34 t1))) ))
(assert (=> (and (laB_1 q1_T0_S34 t1) (and (tok_ t1) (g_ t1)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t1 false false true (sends_ t1))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t1 false false true (sends_ t1))) (laC_1 q1_T0_S34 t1))) ))
(assert (=> (and (laB_1 q1_T0_S34 t1) (and (not (tok_ t1)) (g_ t1)) )  (and (laB_1 q1_T1_S35 (tau_sch_1 t1 false false false (sends_ t1))) (>= (laC_1 q1_T1_S35 (tau_sch_1 t1 false false false (sends_ t1))) (laC_1 q1_T0_S34 t1))) ))
(assert (=> (and (laB_1 q1_T0_S34 t1) (and (not (tok_ t1)) (g_ t1)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t1 false false false (sends_ t1))) (> (laC_1 q1_accept_S34 (tau_sch_1 t1 false false false (sends_ t1))) (laC_1 q1_T0_S34 t1))) ))
(assert (=> (and (laB_1 q1_T0_S34 t2) (and (not (tok_ t2)) (g_ t2)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t2 false false true (sends_ t2))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t2 false false true (sends_ t2))) (laC_1 q1_T0_S34 t2))) ))
(assert (=> (and (laB_1 q1_T0_S34 t2) (and (not (tok_ t2)) (g_ t2)) )  (and (laB_1 q1_T0_S35 (tau_sch_1 t2 false false true (sends_ t2))) (>= (laC_1 q1_T0_S35 (tau_sch_1 t2 false false true (sends_ t2))) (laC_1 q1_T0_S34 t2))) ))
(assert (=> (and (laB_1 q1_T0_S34 t2) (and (tok_ t2) (g_ t2)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t2 false false false (sends_ t2))) (> (laC_1 q1_accept_S34 (tau_sch_1 t2 false false false (sends_ t2))) (laC_1 q1_T0_S34 t2))) ))
(assert (=> (and (laB_1 q1_T0_S34 t2) (and (tok_ t2) (g_ t2)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t2 false false true (sends_ t2))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t2 false false true (sends_ t2))) (laC_1 q1_T0_S34 t2))) ))
(assert (=> (and (laB_1 q1_T0_S34 t2) (and (not (tok_ t2)) (g_ t2)) )  (and (laB_1 q1_T1_S35 (tau_sch_1 t2 false false false (sends_ t2))) (>= (laC_1 q1_T1_S35 (tau_sch_1 t2 false false false (sends_ t2))) (laC_1 q1_T0_S34 t2))) ))
(assert (=> (and (laB_1 q1_T0_S34 t2) (and (not (tok_ t2)) (g_ t2)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t2 false false false (sends_ t2))) (> (laC_1 q1_accept_S34 (tau_sch_1 t2 false false false (sends_ t2))) (laC_1 q1_T0_S34 t2))) ))
(assert (=> (and (laB_1 q1_accept_S34 t0) (and (not (tok_ t0)) (g_ t0)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t0 false false true (sends_ t0))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t0 false false true (sends_ t0))) (laC_1 q1_accept_S34 t0))) ))
(assert (=> (and (laB_1 q1_accept_S34 t0) (and (not (tok_ t0)) (g_ t0)) )  (and (laB_1 q1_T0_S35 (tau_sch_1 t0 false false true (sends_ t0))) (>= (laC_1 q1_T0_S35 (tau_sch_1 t0 false false true (sends_ t0))) (laC_1 q1_accept_S34 t0))) ))
(assert (=> (and (laB_1 q1_accept_S34 t0) (and (tok_ t0) (g_ t0)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t0 false false false (sends_ t0))) (> (laC_1 q1_accept_S34 (tau_sch_1 t0 false false false (sends_ t0))) (laC_1 q1_accept_S34 t0))) ))
(assert (=> (and (laB_1 q1_accept_S34 t0) (and (tok_ t0) (g_ t0)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t0 false false true (sends_ t0))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t0 false false true (sends_ t0))) (laC_1 q1_accept_S34 t0))) ))
(assert (=> (and (laB_1 q1_accept_S34 t0) (and (not (tok_ t0)) (g_ t0)) )  (and (laB_1 q1_T1_S35 (tau_sch_1 t0 false false false (sends_ t0))) (>= (laC_1 q1_T1_S35 (tau_sch_1 t0 false false false (sends_ t0))) (laC_1 q1_accept_S34 t0))) ))
(assert (=> (and (laB_1 q1_accept_S34 t0) (and (not (tok_ t0)) (g_ t0)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t0 false false false (sends_ t0))) (> (laC_1 q1_accept_S34 (tau_sch_1 t0 false false false (sends_ t0))) (laC_1 q1_accept_S34 t0))) ))
(assert (=> (and (laB_1 q1_accept_S34 t1) (and (not (tok_ t1)) (g_ t1)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t1 false false true (sends_ t1))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t1 false false true (sends_ t1))) (laC_1 q1_accept_S34 t1))) ))
(assert (=> (and (laB_1 q1_accept_S34 t1) (and (not (tok_ t1)) (g_ t1)) )  (and (laB_1 q1_T0_S35 (tau_sch_1 t1 false false true (sends_ t1))) (>= (laC_1 q1_T0_S35 (tau_sch_1 t1 false false true (sends_ t1))) (laC_1 q1_accept_S34 t1))) ))
(assert (=> (and (laB_1 q1_accept_S34 t1) (and (tok_ t1) (g_ t1)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t1 false false false (sends_ t1))) (> (laC_1 q1_accept_S34 (tau_sch_1 t1 false false false (sends_ t1))) (laC_1 q1_accept_S34 t1))) ))
(assert (=> (and (laB_1 q1_accept_S34 t1) (and (tok_ t1) (g_ t1)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t1 false false true (sends_ t1))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t1 false false true (sends_ t1))) (laC_1 q1_accept_S34 t1))) ))
(assert (=> (and (laB_1 q1_accept_S34 t1) (and (not (tok_ t1)) (g_ t1)) )  (and (laB_1 q1_T1_S35 (tau_sch_1 t1 false false false (sends_ t1))) (>= (laC_1 q1_T1_S35 (tau_sch_1 t1 false false false (sends_ t1))) (laC_1 q1_accept_S34 t1))) ))
(assert (=> (and (laB_1 q1_accept_S34 t1) (and (not (tok_ t1)) (g_ t1)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t1 false false false (sends_ t1))) (> (laC_1 q1_accept_S34 (tau_sch_1 t1 false false false (sends_ t1))) (laC_1 q1_accept_S34 t1))) ))
(assert (=> (and (laB_1 q1_accept_S34 t2) (and (not (tok_ t2)) (g_ t2)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t2 false false true (sends_ t2))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t2 false false true (sends_ t2))) (laC_1 q1_accept_S34 t2))) ))
(assert (=> (and (laB_1 q1_accept_S34 t2) (and (not (tok_ t2)) (g_ t2)) )  (and (laB_1 q1_T0_S35 (tau_sch_1 t2 false false true (sends_ t2))) (>= (laC_1 q1_T0_S35 (tau_sch_1 t2 false false true (sends_ t2))) (laC_1 q1_accept_S34 t2))) ))
(assert (=> (and (laB_1 q1_accept_S34 t2) (and (tok_ t2) (g_ t2)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t2 false false false (sends_ t2))) (> (laC_1 q1_accept_S34 (tau_sch_1 t2 false false false (sends_ t2))) (laC_1 q1_accept_S34 t2))) ))
(assert (=> (and (laB_1 q1_accept_S34 t2) (and (tok_ t2) (g_ t2)) )  (and (laB_1 q1_T0_S34 (tau_sch_1 t2 false false true (sends_ t2))) (>= (laC_1 q1_T0_S34 (tau_sch_1 t2 false false true (sends_ t2))) (laC_1 q1_accept_S34 t2))) ))
(assert (=> (and (laB_1 q1_accept_S34 t2) (and (not (tok_ t2)) (g_ t2)) )  (and (laB_1 q1_T1_S35 (tau_sch_1 t2 false false false (sends_ t2))) (>= (laC_1 q1_T1_S35 (tau_sch_1 t2 false false false (sends_ t2))) (laC_1 q1_accept_S34 t2))) ))
(assert (=> (and (laB_1 q1_accept_S34 t2) (and (not (tok_ t2)) (g_ t2)) )  (and (laB_1 q1_accept_S34 (tau_sch_1 t2 false false false (sends_ t2))) (> (laC_1 q1_accept_S34 (tau_sch_1 t2 false false false (sends_ t2))) (laC_1 q1_accept_S34 t2))) ))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t0)  (not (tok_ t0))  )  (laB_1 q1_T6_S11 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t0)  (not (tok_ t0))  )  (laB_1 q1_T0_S11 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t0) (and (not (sends_ t0)) (tok_ t0)) )  (laB_1 q1_T0_S37 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t0)  )  (laB_1 q1_T0_S19 (tau_sch_1 t0 ?r0 false true (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t0) (and (not (sends_ t0)) (tok_ t0)) )  (laB_1 q1_T1_S37 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t0)  )  (laB_1 q1_T1_S19 (tau_sch_1 t0 ?r0 false false (sends_ t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t1)  (not (tok_ t1))  )  (laB_1 q1_T6_S11 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t1)  (not (tok_ t1))  )  (laB_1 q1_T0_S11 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t1) (and (not (sends_ t1)) (tok_ t1)) )  (laB_1 q1_T0_S37 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t1)  )  (laB_1 q1_T0_S19 (tau_sch_1 t1 ?r0 false true (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t1) (and (not (sends_ t1)) (tok_ t1)) )  (laB_1 q1_T1_S37 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t1)  )  (laB_1 q1_T1_S19 (tau_sch_1 t1 ?r0 false false (sends_ t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t2)  (not (tok_ t2))  )  (laB_1 q1_T6_S11 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t2)  (not (tok_ t2))  )  (laB_1 q1_T0_S11 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t2) (and (not (sends_ t2)) (tok_ t2)) )  (laB_1 q1_T0_S37 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t2)  )  (laB_1 q1_T0_S19 (tau_sch_1 t2 ?r0 false true (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t2) (and (not (sends_ t2)) (tok_ t2)) )  (laB_1 q1_T1_S37 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S19 t2)  )  (laB_1 q1_T1_S19 (tau_sch_1 t2 ?r0 false false (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S17 t0)  (not (g_ t0))  )  (laB_1 q1_T4_S17 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S17 t0) (and (not (tok_ t0)) (g_ t0)) )  (laB_1 q1_accept_S7 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S17 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (laB_1 q1_T4_S8 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S17 t0)  (g_ t0)  )  (laB_1 q1_T0_S16 (tau_sch_1 t0 false false ?sch0 (sends_ t0))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S17 t1)  (not (g_ t1))  )  (laB_1 q1_T4_S17 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S17 t1) (and (not (tok_ t1)) (g_ t1)) )  (laB_1 q1_accept_S7 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S17 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (laB_1 q1_T4_S8 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S17 t1)  (g_ t1)  )  (laB_1 q1_T0_S16 (tau_sch_1 t1 false false ?sch0 (sends_ t1))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S17 t2)  (not (g_ t2))  )  (laB_1 q1_T4_S17 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S17 t2) (and (not (tok_ t2)) (g_ t2)) )  (laB_1 q1_accept_S7 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S17 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (laB_1 q1_T4_S8 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool)) (=> (and (laB_1 q1_T4_S17 t2)  (g_ t2)  )  (laB_1 q1_T0_S16 (tau_sch_1 t2 false false ?sch0 (sends_ t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S37 t0)  (not (sends_ t0))  )  (and (laB_1 q1_T1_S37 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) (>= (laC_1 q1_T1_S37 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) (laC_1 q1_T1_S37 t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S37 t0) (and (not (sends_ t0)) (not (tok_ t0))) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) (> (laC_1 q1_accept_S10 (tau_sch_1 t0 ?r0 false ?sch0 (sends_ t0))) (laC_1 q1_T1_S37 t0))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S37 t1)  (not (sends_ t1))  )  (and (laB_1 q1_T1_S37 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) (>= (laC_1 q1_T1_S37 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) (laC_1 q1_T1_S37 t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S37 t1) (and (not (sends_ t1)) (not (tok_ t1))) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) (> (laC_1 q1_accept_S10 (tau_sch_1 t1 ?r0 false ?sch0 (sends_ t1))) (laC_1 q1_T1_S37 t1))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S37 t2)  (not (sends_ t2))  )  (and (laB_1 q1_T1_S37 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) (>= (laC_1 q1_T1_S37 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) (laC_1 q1_T1_S37 t2))) )))
(assert (forall ((?sch0 Bool) (?r0 Bool)) (=> (and (laB_1 q1_T1_S37 t2) (and (not (sends_ t2)) (not (tok_ t2))) )  (and (laB_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) (> (laC_1 q1_accept_S10 (tau_sch_1 t2 ?r0 false ?sch0 (sends_ t2))) (laC_1 q1_T1_S37 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t0) (and (tok_ t0) (not (g_ t0))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S25 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S25 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t0) (and (tok_ t0) (not (g_ t0))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S25 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (> (laC_1 q1_accept_S25 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S25 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (and (laB_1 q1_T1_S27 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (>= (laC_1 q1_T1_S27 (tau_sch_1 t0 ?r0 false false (sends_ t0))) (laC_1 q1_T0_S25 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (and (laB_1 q1_T0_S27 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S27 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S25 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t0) (and (not (tok_ t0)) (not (g_ t0))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t0 ?r0 false true (sends_ t0))) (laC_1 q1_T0_S25 t0))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t1) (and (tok_ t1) (not (g_ t1))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S25 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S25 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t1) (and (tok_ t1) (not (g_ t1))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S25 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (> (laC_1 q1_accept_S25 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S25 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (and (laB_1 q1_T1_S27 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (>= (laC_1 q1_T1_S27 (tau_sch_1 t1 ?r0 false false (sends_ t1))) (laC_1 q1_T0_S25 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (and (laB_1 q1_T0_S27 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S27 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S25 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t1) (and (not (tok_ t1)) (not (g_ t1))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t1 ?r0 false true (sends_ t1))) (laC_1 q1_T0_S25 t1))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t2) (and (tok_ t2) (not (g_ t2))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S25 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S25 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t2) (and (tok_ t2) (not (g_ t2))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S25 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (and (laB_1 q1_accept_S25 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (> (laC_1 q1_accept_S25 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S25 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (and (laB_1 q1_T1_S27 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (>= (laC_1 q1_T1_S27 (tau_sch_1 t2 ?r0 false false (sends_ t2))) (laC_1 q1_T0_S25 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (and (laB_1 q1_T0_S27 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S27 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S25 t2))) )))
(assert (forall ((?r0 Bool)) (=> (and (laB_1 q1_T0_S25 t2) (and (not (tok_ t2)) (not (g_ t2))) )  (and (laB_1 q1_T0_S25 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (>= (laC_1 q1_T0_S25 (tau_sch_1 t2 ?r0 false true (sends_ t2))) (laC_1 q1_T0_S25 t2))) )))

; end of 'bad assertions' section


(check-sat)

